A, B:Top List. null(B)  (last(A @ B) ~ last(B)) 

latex

Definitions	Top, t  T, x:A. B(x), null(as), b, A, P  Q, as @ bs, Prop, b, , P & Q, P  Q, Unit, False
Lemmas	append is nil, last-cons, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of null, bool wf, bnot wf, append wf, not wf, assert wf, null wf3, top wf